﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using TruthTree2.PC.Logic;
using TruthTree2.PC.Resolution;

namespace TruthTree2.Extensions
{
    public static class CNFExtensions
    {
        #region eliminateConditionals
        private static Sentence eliminateConditionals(Sentence s)
        {
            if (s is Atom) { return eliminateConditionals((Atom)s); }
            else if (s is Biconditional) { return eliminateConditionals((Biconditional)s); }
            else if (s is Conditional) { return eliminateConditionals((Conditional)s); }
            else if (s is Conjunction) { return eliminateConditionals((Conjunction)s); }
            else if (s is Disjunction) { return eliminateConditionals((Disjunction)s); }
            else if (s is Negation) { return eliminateConditionals((Negation)s); }

            throw new NotImplementedException(s.GetType().ToString());
        }
        private static Sentence eliminateConditionals(Atom a)
        {
            if (a is Constant) { return eliminateConditionals((Constant)a); }

            throw new NotImplementedException(a.GetType().ToString());
        }
        private static Sentence eliminateConditionals(Biconditional b)
        {
            Sentence left = new Conditional(b.left.Copy(), b.right.Copy());
            Sentence right = new Conditional(b.right.Copy(), b.left.Copy());

            return new Conjunction(
                eliminateConditionals(left),
                eliminateConditionals(right));
        }
        private static Sentence eliminateConditionals(Conditional c)
        {
            return new Disjunction(
                new Negation(eliminateConditionals(c.antecedent.Copy())),
                eliminateConditionals(c.consequent.Copy()));
        }
        private static Sentence eliminateConditionals(Conjunction c)
        {
            return new Conjunction(
                eliminateConditionals(c.left.Copy()),
                eliminateConditionals(c.right.Copy()));
        }
        private static Sentence eliminateConditionals(Constant c)
        {
            return c.Copy();
        }
        private static Sentence eliminateConditionals(Disjunction d)
        {
            return new Disjunction(
                eliminateConditionals(d.left.Copy()),
                eliminateConditionals(d.right.Copy()));
        }
        private static Sentence eliminateConditionals(Negation n)
        {
            return new Negation(eliminateConditionals(n.inner.Copy()));
        }
        #endregion
        #region moveNotsInwards
        private static Sentence moveNotsInwards(Sentence s)
        {
            if (s is Atom) { return moveNotsInwards((Atom)s); }
            else if (s is Conjunction) { return moveNotsInwards((Conjunction)s); }
            else if (s is Disjunction) { return moveNotsInwards((Disjunction)s); }
            else if (s is Negation) { return moveNotsInwards((Negation)s); }

            throw new NotImplementedException(s.GetType().ToString());
        }
        private static Sentence moveNotsInwards(Atom a)
        {
            if (a is Constant) { return moveNotsInwards((Constant)a); }

            throw new NotImplementedException(a.GetType().ToString());
        }
        private static Sentence moveNotsInwards(Conjunction c)
        {
            return new Conjunction(
                moveNotsInwards(c.left.Copy()),
                moveNotsInwards(c.right.Copy()));
        }
        private static Sentence moveNotsInwards(Constant c)
        {
            return c.Copy();
        }
        private static Sentence moveNotsInwards(Disjunction d)
        {
            return new Disjunction(
                moveNotsInwards(d.left.Copy()),
                moveNotsInwards(d.right.Copy()));
        }
        private static Sentence moveNotsInwards(Negation n)
        {
            if (n.inner is Conjunction)
            {
                Conjunction inner = (Conjunction)n.inner;
                Sentence left = inner.left.GetNegation();
                Sentence right = inner.right.GetNegation();

                return new Disjunction(
                    moveNotsInwards(left),
                    moveNotsInwards(right));
            }
            else if (n.inner is Disjunction)
            {
                Disjunction inner = (Disjunction)n.inner;
                Sentence left = inner.left.GetNegation();
                Sentence right = inner.right.GetNegation();

                return new Conjunction(
                    moveNotsInwards(left),
                    moveNotsInwards(right));
            }
            else if (n.inner is Negation)
            {
                Negation inner = (Negation)n.inner;
                return inner.inner.Copy();
            }

            return n.Copy();
        }
        #endregion
        #region distributeOrsOverAnds
        private static Sentence distributeOrsOverAnds(Sentence s)
        {
            if (s is Atom) { return distributeOrsOverAnds((Atom)s); }
            else if (s is Conjunction) { return distributeOrsOverAnds((Conjunction)s); }
            else if (s is Disjunction) { return distributeOrsOverAnds((Disjunction)s); }
            else if (s is Negation) { return distributeOrsOverAnds((Negation)s); }

            throw new NotImplementedException(s.GetType().ToString());
        }
        private static Sentence distributeOrsOverAnds(Atom a)
        {
            if (a is Constant) { return distributeOrsOverAnds((Constant)a); }

            throw new NotImplementedException(a.GetType().ToString());
        }
        private static Sentence distributeOrsOverAnds(Conjunction c)
        {
            return new Conjunction(
                distributeOrsOverAnds(c.left.Copy()),
                distributeOrsOverAnds(c.right.Copy()));
        }
        private static Sentence distributeOrsOverAnds(Constant c)
        {
            return c.Copy();
        }
        private static Sentence distributeOrsOverAnds(Disjunction d)
        {
            if (d.left is Conjunction)
            {
                Conjunction c = (Conjunction)d.left;
                Sentence left = new Disjunction(d.right.Copy(), c.left.Copy());
                Sentence right = new Disjunction(d.right.Copy(), c.right.Copy());

                return new Conjunction(
                    distributeOrsOverAnds(left),
                    distributeOrsOverAnds(right));
            }
            if (d.right is Conjunction)
            {
                Conjunction c = (Conjunction)d.right;
                Sentence left = new Disjunction(d.left.Copy(), c.left.Copy());
                Sentence right = new Disjunction(d.left.Copy(), c.right.Copy());

                return new Conjunction(
                    distributeOrsOverAnds(left),
                    distributeOrsOverAnds(right));
            }

            return new Disjunction(
                distributeOrsOverAnds(d.left.Copy()),
                distributeOrsOverAnds(d.right.Copy()));
        }
        private static Sentence distributeOrsOverAnds(Negation n)
        {
            return distributeOrsOverAnds(n.inner.Copy()).GetNegation();
        }
        #endregion

        public static Sentence ConvertToNNF(this Sentence s)
        {
            Sentence res = eliminateConditionals(s);
            res = moveNotsInwards(res);

            return res;
        }

        public static Sentence ConvertToCNFSentence(this Sentence s)
        {
            Sentence nnf = ConvertToNNF(s);

            // standardize variables
            // skolemize
            // drop quantifiers

            Sentence dis = distributeOrsOverAnds(nnf);
            return dis;
        }

        private static CNFAtom atomToCNF(Atom a, bool neg = false)
        {
            if (a is Constant)
            {
                Constant c = (Constant)a;
                return new CNFAtom()
                {
                    Negated = neg,
                    Atom = c.label
                };
            }

            throw new Exception("Fail");
        }

        public static CNFSet ConvertToCNF(this Sentence s)
        {
            if (s is Conjunction)
            {
                Conjunction c = (Conjunction)s;

                return CNFSet.Union(c.left.ConvertToCNF(), c.right.ConvertToCNF());
            }
            else if (s is Disjunction)
            {
                Disjunction d = (Disjunction)s;
                CNFClause clause = new CNFClause();
                if (d.left is Negation)
                {
                    Negation n = (Negation)d.left;
                    clause.Atoms.Add(atomToCNF((Atom)n.inner, true));
                }
                else if (d.left is Atom)
                {
                    clause.Atoms.Add(atomToCNF((Atom)d.left, false));
                }
                if (d.right is Negation)
                {
                    Negation n = (Negation)d.right;
                    clause.Atoms.Add(atomToCNF((Atom)n.inner, true));
                }
                else if (d.right is Atom)
                {
                    clause.Atoms.Add(atomToCNF((Atom)d.right, false));
                }

                CNFSet res = new CNFSet();
                res.Clauses.Add(clause);
                return res;
            }
            else if (s is Negation)
            {
                Negation n = (Negation)s;
                if (n.inner is Atom)
                {
                    CNFAtom atom = atomToCNF((Atom)n.inner, true);
                    CNFClause clause = new CNFClause();
                    clause.Atoms.Add(atom);
                    CNFSet res = new CNFSet();
                    res.Clauses.Add(clause);
                    return res;
                }
            }
            else if (s is Atom)
            {
                CNFAtom atom = atomToCNF((Atom)s, false);
                CNFClause clause = new CNFClause();
                clause.Atoms.Add(atom);
                CNFSet res = new CNFSet();
                res.Clauses.Add(clause);
                return res;
            }

            throw new Exception("Dunno what happened there");
        }
    }
}
